$\forall$$A$:Type, $R$:($A$$\rightarrow$Realizer), $i$:Id, $L$:($A$ List).
\\[0ex]($\uparrow$R{-}has{-}loc($\oplus$$x$$\in$$L$.$R$($x$);$i$)) $\Leftarrow\!\Rightarrow$ ($\exists$$x$$\in$$L$.$\uparrow$R{-}has{-}loc($R$($x$);$i$))